//This file was generated from (Academic) UPPAAL 4.1.18 (rev. 5444), November 2013

/*

*/
E<> ticketcpu

/*

*/
E<> ticketdegrade

/*

*/
E<> ticketdown

/*

*/
E<> ticketfull

/*
true: the two ticket can co-exist sometimes
*/
A[] ! (ticketdown && ticketdegrade)

/*
true: the two tickets don't cohexist for more than 120 sec
*/
A[] ! (ticketdegrade && ticketcpu && cTicketCPU > 120)

/*
false: the two tickets can cohexist
*/
A[] ! (ticketdegrade && ticketcpu)

/*
true: a ticket degrade and a ticket full can co-exist only for 120 time units
*/
A[] ! (ticketdegrade && ticketfull && cTicketFull > 120)

/*
false: a degrade ticket can be opened, before detecting its because of full band
*/
A[] ! (ticketdegrade && ticketfull)

/*
true
*/
A[] ! (ticketdown && ticketfull)

/*

*/
E<> ! deadlock

/*

*/
A[] ! deadlock
